File: dummy_funs.ml

package info (click to toggle)
hol88 2.02.19940316-15
  • links: PTS
  • area: main
  • in suites: wheezy
  • size: 65,928 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,075; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (17 lines) | stat: -rw-r--r-- 737 bytes parent folder | download | duplicates (11) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
 
% ===================================================================== %
% FILE: dummy_funs.ml 	DATE: 16 July 93    BY: Wai WONG		%
% Define some dummy functions to be used when not in recording		%
% ===================================================================== %

let new_proof_file (s:string) = ()
and close_proof_file (():void) = ()
and begin_proof (s:string) = ()
and end_proof (():void) = ()
and current_proof (():void) = ``
and current_proof_file (():void) = ``
and (write_proof_add_to:(string -> string -> thm list -> * list -> void))
     s s' thml lnl = ()
and (write_proof_to:(string -> string -> thm list -> * list -> void))
     s s' thml lnl = ()
and (write_last_proof : (string -> thm list -> void)) s thl = ();;