# HG changeset patch
# User clasohm
# Date 814543082 -3600
# Node ID 7ac266cf82d08b9ac34585593144c8fabf4ce736
# Parent  ae31bb7774a7e1d5c9cfd00444b6b5f3d7ef41b2
added calls of init_html and make_chart;
added usage of qed to LK.ML

diff -r ae31bb7774a7 -r 7ac266cf82d0 src/LK/LK.ML
--- a/src/LK/LK.ML	Tue Oct 24 14:50:24 1995 +0100
+++ b/src/LK/LK.ML	Tue Oct 24 14:58:02 1995 +0100
@@ -11,45 +11,6 @@
 (*Higher precedence than := facilitates use of references*)
 infix 4 add_safes add_unsafes;
 
-signature LK_RESOLVE = 
-  sig
-  datatype pack = Pack of thm list * thm list
-  val add_safes:   pack * thm list -> pack
-  val add_unsafes: pack * thm list -> pack
-  val allL_thin: thm
-  val best_tac: pack -> int -> tactic
-  val could_res: term * term -> bool
-  val could_resolve_seq: term * term -> bool
-  val cutL_tac: string -> int -> tactic
-  val cutR_tac: string -> int -> tactic
-  val conL: thm
-  val conR: thm
-  val empty_pack: pack
-  val exR_thin: thm
-  val fast_tac: pack -> int -> tactic
-  val filseq_resolve_tac: thm list -> int -> int -> tactic
-  val forms_of_seq: term -> term list
-  val has_prems: int -> thm -> bool   
-  val iffL: thm
-  val iffR: thm
-  val less: thm * thm -> bool
-  val LK_dup_pack: pack
-  val LK_pack: pack
-  val pc_tac: pack -> int -> tactic
-  val prop_pack: pack
-  val repeat_goal_tac: pack -> int -> tactic
-  val reresolve_tac: thm list -> int -> tactic   
-  val RESOLVE_THEN: thm list -> (int -> tactic) -> int -> tactic   
-  val safe_goal_tac: pack -> int -> tactic
-  val step_tac: pack -> int -> tactic
-  val symL: thm
-  val TrueR: thm
-  end;
-
-
-structure LK_Resolve : LK_RESOLVE = 
-struct
-
 (*Cut and thin, replacing the right-side formula*)
 fun cutR_tac (sP: string) i = 
     res_inst_tac [ ("P",sP) ] cut i  THEN  rtac thinR i;
@@ -60,31 +21,31 @@
 
 
 (** If-and-only-if rules **)
-val iffR = prove_goalw LK.thy [iff_def]
+qed_goalw "iffR" LK.thy [iff_def]
     "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[conjR,impR]) 1)) ]);
 
-val iffL = prove_goalw LK.thy [iff_def]
+qed_goalw "iffL" LK.thy [iff_def]
    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
  (fn prems=> [ (REPEAT (resolve_tac (prems@[conjL,impL,basic]) 1)) ]);
 
-val TrueR = prove_goalw LK.thy [True_def]
+qed_goalw "TrueR" LK.thy [True_def]
     "$H |- $E, True, $F"
  (fn _=> [ rtac impR 1, rtac basic 1 ]);
 
 
 (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
 
-val allL_thin = prove_goal LK.thy 
+qed_goal "allL_thin" LK.thy 
     "$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E"
  (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);
 
-val exR_thin = prove_goal LK.thy 
+qed_goal "exR_thin" LK.thy 
     "$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F"
  (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);
 
 (* Symmetry of equality in hypotheses *)
-val symL = prove_goal LK.thy 
+qed_goal "symL" LK.thy 
     "$H, $G, B = A |- $E ==> $H, A = B, $G |- $E" 
  (fn prems=>
   [ (rtac cut 1),
@@ -222,16 +183,12 @@
 
 (** Contraction.  Useful since some rules are not complete. **)
 
-val conR = prove_goal LK.thy 
+qed_goal "conR" LK.thy 
     "$H |- $E, P, $F, P ==> $H |- $E, P, $F"
  (fn prems=>
   [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
 
-val conL = prove_goal LK.thy 
+qed_goal "conL" LK.thy 
     "$H, P, $G, P |- $E ==> $H, P, $G |- $E"
  (fn prems=>
   [ (rtac cut 1), (REPEAT (resolve_tac (prems@[basic]) 1)) ]);
-
-end;
-
-open LK_Resolve;
diff -r ae31bb7774a7 -r 7ac266cf82d0 src/LK/Makefile
--- a/src/LK/Makefile	Tue Oct 24 14:50:24 1995 +0100
+++ b/src/LK/Makefile	Tue Oct 24 14:58:02 1995 +0100
@@ -1,3 +1,4 @@
+# $Id$
 #########################################################################
 #									#
 # 			Makefile for Isabelle (LK)			#
@@ -5,9 +6,11 @@
 #########################################################################
 
 #To make the system, cd to this directory and type  
-#	make -f Makefile 
+#	make
 #To make the system and test it on standard examples, type  
-#	make -f Makefile test
+#	make test
+#To generate HTML files for every theory, set the environment variable
+#MAKE_HTML or add the parameter "MAKE_HTML=".
 
 #Environment variable ISABELLECOMP specifies the compiler.
 #Environment variable ISABELLEBIN specifies the destination directory.
@@ -25,8 +28,16 @@
 	case "$(COMP)" in \
 	poly*)	echo 'make_database"$(BIN)/LK"; quit();'  \
 			| $(COMP) $(BIN)/Pure;\
-		echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LK ;;\
-	sml*)	echo 'exit_use"ROOT.ML"; xML"$(BIN)/LK" banner;' | $(BIN)/Pure ;;\
+                if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+                then echo 'open PolyML; init_html (); exit_use"ROOT";' \
+                       | $(COMP) $(BIN)/LK;\
+		else echo 'open PolyML; exit_use"ROOT";' | $(COMP) $(BIN)/LK;\
+                fi;;\
+	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ];\
+                then echo 'init_html (); exit_use"ROOT.ML";                                               xML"$(BIN)/LK" banner;' | $(BIN)/Pure;\
+                else echo 'exit_use"ROOT.ML"; xML"$(BIN)/LK" banner;' \
+                       | $(BIN)/Pure;\
+                fi;;\
 	*)	echo Bad value for ISABELLECOMP: \
                 	$(COMP) is not poly or sml;;\
 	esac
diff -r ae31bb7774a7 -r 7ac266cf82d0 src/LK/ROOT.ML
--- a/src/LK/ROOT.ML	Tue Oct 24 14:50:24 1995 +0100
+++ b/src/LK/ROOT.ML	Tue Oct 24 14:58:02 1995 +0100
@@ -19,4 +19,6 @@
 use "../Pure/install_pp.ML";
 print_depth 8;
 
+make_chart ();   (*make HTML chart*)
+
 val LK_build_completed = ();	(*indicate successful build*)