Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Many other files modified as follows:
authorlcp
Tue, 18 Jan 1994 15:57:40 +0100
changeset 230 ec8a2b6aa8a7
parent 229 4002c4cd450c
child 231 cb6a24451544
Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g
src/Pure/goals.ML file | annotate | diff | comparison | revisions
src/Pure/install_pp.ML file | annotate | diff | comparison | revisions
src/Pure/tactic.ML file | annotate | diff | comparison | revisions
src/Pure/tctical.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/goals.ML	Tue Jan 18 13:46:08 1994 +0100
+++ b/src/Pure/goals.ML	Tue Jan 18 15:57:40 1994 +0100
@@ -41,7 +41,7 @@
   val gethyps: int -> thm list
   val goal:  theory -> string -> thm list
   val goalw: theory -> thm list -> string -> thm list
-  val goalw_cterm:     thm list -> Sign.cterm -> thm list
+  val goalw_cterm:     thm list -> cterm -> thm list
   val pop_proof: unit -> thm list
   val pr: unit -> unit
   val premises: unit -> thm list
@@ -54,7 +54,7 @@
   val proof_timing: bool ref
   val prove_goal: theory -> string -> (thm list -> tactic list) -> thm
   val prove_goalw: theory->thm list->string->(thm list->tactic list)->thm
-  val prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
+  val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
   val push_proof: unit -> unit
   val read: string -> term
   val ren: string -> int -> unit
@@ -99,7 +99,7 @@
     ref((fn _=> error"No goal has been supplied in subgoal module") 
        : bool*thm->thm);
 
-val dummy = trivial(Sign.read_cterm Sign.pure 
+val dummy = trivial(read_cterm Sign.pure 
     ("PROP No_goal_has_been_supplied",propT));
 
 (*List of previous goal stacks, for the undo operation.  Set by setstate. 
@@ -124,13 +124,13 @@
 (*Common treatment of "goal" and "prove_goal":
   Return assumptions, initial proof state, and function to make result. *)
 fun prepare_proof rths chorn =
-  let val {sign, t=horn,...} = Sign.rep_cterm chorn;
+  let val {sign, t=horn,...} = rep_cterm chorn;
       val (_,As,B) = Logic.strip_horn(horn);
-      val cAs = map (Sign.cterm_of sign) As;
+      val cAs = map (cterm_of sign) As;
       val p_rew = if null rths then I else rewrite_rule rths;
       val c_rew = if null rths then I else rewrite_goals_rule rths;
       val prems = map (p_rew o forall_elim_vars(0) o assume) cAs
-      and st0 = c_rew (trivial (Sign.cterm_of sign B))
+      and st0 = c_rew (trivial (cterm_of sign B))
       fun result_error state msg = 
         (writeln ("Bad final proof state:");
  	 !print_goals_ref (!goals_limit) state;
@@ -151,7 +151,7 @@
                 ("Additional hypotheses:\n" ^ 
                  cat_lines (map (Sign.string_of_term sign) hyps))
 	    else if Pattern.eta_matches (#tsig(Sign.rep_sg sign)) 
-			                (Sign.term_of chorn, prop)
+			                (term_of chorn, prop)
 		 then  standard th 
 	    else  result_error state "proved a different theorem"
         end
@@ -199,7 +199,7 @@
 (*Version taking the goal as a string*)
 fun prove_goalw thy rths agoal tacsf =
   let val sign = sign_of thy
-      val chorn = Sign.read_cterm sign (agoal,propT)
+      val chorn = read_cterm sign (agoal,propT)
   in  prove_goalw_cterm rths chorn tacsf  
       handle ERROR => error (*from type_assign, etc via prepare_proof*)
 		("The error above occurred for " ^ quote agoal)
@@ -286,7 +286,7 @@
     Initial subgoal and premises are rewritten using rths. **)
 
 (*Version taking the goal as a cterm; if you have a term t and theory thy, use
-    goalw_cterm rths (Sign.cterm_of (sign_of thy) t);      *)
+    goalw_cterm rths (cterm_of (sign_of thy) t);      *)
 fun goalw_cterm rths chorn = 
   let val (prems, st0, mkresult) = prepare_proof rths chorn
   in  undo_list := [];
@@ -298,7 +298,7 @@
 
 (*Version taking the goal as a string*)
 fun goalw thy rths agoal = 
-  goalw_cterm rths (Sign.read_cterm(sign_of thy)(agoal,propT))
+  goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT))
   handle ERROR => error (*from type_assign, etc via prepare_proof*)
 	    ("The error above occurred for " ^ quote agoal);
 
@@ -418,7 +418,7 @@
 
 fun top_sg() = #sign(rep_thm(topthm()));
 
-fun read s = Sign.term_of (Sign.read_cterm (top_sg())
+fun read s = term_of (read_cterm (top_sg())
 			                   (s, (TVar(("DUMMY",0),[]))));
 
 (*Print a term under the current signature of the proof state*)
--- a/src/Pure/install_pp.ML	Tue Jan 18 13:46:08 1994 +0100
+++ b/src/Pure/install_pp.ML	Tue Jan 18 15:57:40 1994 +0100
@@ -4,12 +4,12 @@
 Set up automatic toplevel printing
 *)
 
-install_pp (make_pp ["Thm", "thm"] pprint_thm);
-install_pp (make_pp ["Thm", "theory"] pprint_theory);
-install_pp (make_pp ["Sign", "sg"] pprint_sg);
-install_pp (make_pp ["Sign", "cterm"] Sign.pprint_cterm);
-install_pp (make_pp ["Sign", "ctyp"] Sign.pprint_ctyp);
-install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
+install_pp (make_pp ["Thm", "thm"] 	pprint_thm);
+install_pp (make_pp ["Thm", "theory"] 	pprint_theory);
+install_pp (make_pp ["Thm", "cterm"] 	pprint_cterm);
+install_pp (make_pp ["Thm", "ctyp"] 	pprint_ctyp);
+install_pp (make_pp ["Sign", "sg"] 	pprint_sg);
+install_pp (make_pp ["Syntax", "ast"] 	Syntax.pprint_ast);
 
 (*
 install_pp (make_pp ["term"] pprint_term);
--- a/src/Pure/tactic.ML	Tue Jan 18 13:46:08 1994 +0100
+++ b/src/Pure/tactic.ML	Tue Jan 18 15:57:40 1994 +0100
@@ -99,8 +99,8 @@
   let val fth = freezeT th
       val {prop,sign,...} = rep_thm fth
       fun mk_inst (Var(v,T)) = 
-	  (Sign.cterm_of sign (Var(v,T)),
-	   Sign.cterm_of sign (Free(string_of v, T)))
+	  (cterm_of sign (Var(v,T)),
+	   cterm_of sign (Free(string_of v, T)))
       val insts = map mk_inst (term_vars prop)
   in  instantiate ([],insts) fth  end;
 
@@ -184,14 +184,14 @@
     fun liftterm t = list_abs_free (params, 
 				    Logic.incr_indexes(paramTs,inc) t)
     (*Lifts instantiation pair over params*)
-    fun liftpair (cv,ct) = (Sign.cfun liftvar cv, Sign.cfun liftterm ct)
+    fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
     fun lifttvar((a,i),ctyp) =
-	let val {T,sign} = Sign.rep_ctyp ctyp
-	in  ((a,i+inc), Sign.ctyp_of sign (incr_tvar inc T)) end
+	let val {T,sign} = rep_ctyp ctyp
+	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
     val rts = types_sorts rule and (types,sorts) = types_sorts state
     fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
       | types'(ixn) = types ixn;
-    val (Tinsts,insts) = Sign.read_insts sign rts (types',sorts) sinsts
+    val (Tinsts,insts) = read_insts sign rts (types',sorts) sinsts
 in instantiate (map lifttvar Tinsts, map liftpair insts)
 		(lift_rule (state,i) rule)
 end;
--- a/src/Pure/tctical.ML	Tue Jan 18 13:46:08 1994 +0100
+++ b/src/Pure/tctical.ML	Tue Jan 18 15:57:40 1994 +0100
@@ -399,7 +399,7 @@
 (* (!!x. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
 val dummy_quant_rl = 
   standard (forall_elim_var 0 (assume 
-                  (Sign.read_cterm Sign.pure ("!!x::prop. PROP V",propT))));
+                  (read_cterm Sign.pure ("!!x::prop. PROP V",propT))));
 
 (* Prevent the subgoal's assumptions from becoming additional subgoals in the
    new proof state by enclosing them by a universal quantification *)
@@ -411,7 +411,7 @@
 (*Does the work of SELECT_GOAL. *)
 fun select (Tactic tf) state i =
   let val prem::_ = drop(i-1, prems_of state)
-      val st0 = trivial (Sign.cterm_of (#sign(rep_thm state)) prem);
+      val st0 = trivial (cterm_of (#sign(rep_thm state)) prem);
       fun next st = bicompose false (false, st, nprems_of st) i state
   in  Sequence.flats (Sequence.maps next (tf st0))
   end;
@@ -469,7 +469,7 @@
 
 fun metahyps_aux_tac tacf (prem,i) = Tactic (fn state =>
   let val {sign,maxidx,...} = rep_thm state
-      val cterm = Sign.cterm_of sign
+      val cterm = cterm_of sign
       (*find all vars in the hyps -- should find tvars also!*)
       val hyps_vars = foldr add_term_vars (strip_assums_hyp prem, [])
       val insts = map mk_inst hyps_vars
isabelle