# HG changeset patch
# User wenzelm
# Date 1563825302 -7200
# Node ID f5bce5af361b4d9a00d9ce2ca06ff2cbd34b43ef
# Parent  425c5f9bc61a01e51df106e3b9003f9150d7131f
tuned comments -- proper sections;

diff -r 425c5f9bc61a -r f5bce5af361b src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Mon Jul 22 16:15:40 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Mon Jul 22 21:55:02 2019 +0200
@@ -34,7 +34,7 @@
   (vars_of prop @ frees_of prop) prf;
 
 
-(**** generate constraints for proof term ****)
+(* generate constraints for proof term *)
 
 fun mk_var env Ts T =
   let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
@@ -231,7 +231,7 @@
   in mk_cnstrts env [] [] Symtab.empty cprf end;
 
 
-(**** update list of free variables of constraints ****)
+(* update list of free variables of constraints *)
 
 fun upd_constrs env cs =
   let
@@ -252,7 +252,7 @@
   in check_cs cs end;
 
 
-(**** solution of constraints ****)
+(* solution of constraints *)
 
 fun solve _ [] bigenv = bigenv
   | solve ctxt cs bigenv =
@@ -284,7 +284,7 @@
       end;
 
 
-(**** reconstruction of proofs ****)
+(* reconstruction of proofs *)
 
 fun reconstruct_proof ctxt prop cprf =
   let
@@ -335,8 +335,7 @@
   in reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
 
 
-
-(**** expand and reconstruct subproofs ****)
+(* expand and reconstruct subproofs *)
 
 fun expand_proof ctxt thms prf =
   let
diff -r 425c5f9bc61a -r f5bce5af361b src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 22 16:15:40 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 22 21:55:02 2019 +0200
@@ -61,7 +61,7 @@
   val decode: proof XML.Decode.T
   val decode_body: proof_body XML.Decode.T
 
-  (** primitive operations **)
+  (*primitive operations*)
   val proofs_enabled: unit -> bool
   val atomic_proof: proof -> bool
   val compact_proof: proof -> bool
@@ -95,7 +95,7 @@
   val proofT: typ
   val term_of_proof: proof -> term
 
-  (** proof terms for specific inference rules **)
+  (*proof terms for specific inference rules*)
   val implies_intr_proof: term -> proof -> proof
   val implies_intr_proof': term -> proof -> proof
   val forall_intr_proof: term -> string -> proof -> proof
@@ -139,7 +139,7 @@
   val oracle_proof: string -> term -> oracle * proof
   val shrink_proof: proof -> proof
 
-  (** rewriting on proof terms **)
+  (*rewriting on proof terms*)
   val add_prf_rrule: proof * proof -> theory -> theory
   val add_prf_rproc: (typ list -> term option list -> proof -> (proof * proof) option) -> theory -> theory
   val no_skel: proof
@@ -163,7 +163,7 @@
 structure Proofterm : PROOFTERM =
 struct
 
-(***** datatype proof *****)
+(** datatype proof **)
 
 datatype proof =
    MinProof
@@ -215,7 +215,7 @@
         in consolidate (join_thms thms) end)};
 
 
-(***** proof atoms *****)
+(* proof atoms *)
 
 fun fold_proof_atoms all f =
   let
@@ -314,7 +314,8 @@
   | no_thm_proofs a = a;
 
 
-(***** XML data representation *****)
+
+(** XML data representation **)
 
 (* encode *)
 
@@ -386,7 +387,7 @@
 end;
 
 
-(***** proof objects with different levels of detail *****)
+(** proof objects with different levels of detail **)
 
 fun atomic_proof prf =
   (case prf of
@@ -492,7 +493,7 @@
   | change_type _ prf = prf;
 
 
-(***** utilities *****)
+(* utilities *)
 
 fun strip_abs (_::Ts) (Abs (_, _, t)) = strip_abs Ts t
   | strip_abs _ t = t;
@@ -591,7 +592,7 @@
   | prf_add_loose_bnos _ _ _ _ = ([], []);
 
 
-(**** substitutions ****)
+(* substitutions *)
 
 fun del_conflicting_tvars envT T = Term_Subst.instantiateT
   (map_filter (fn ixnS as (_, S) =>
@@ -643,7 +644,7 @@
   in Same.commit norm end;
 
 
-(***** Remove some types in proof term (to save space) *****)
+(* remove some types in proof term (to save space) *)
 
 fun remove_types (Abs (s, _, t)) = Abs (s, dummyT, remove_types t)
   | remove_types (t $ u) = remove_types t $ remove_types u
@@ -656,7 +657,7 @@
 fun norm_proof' env prf = norm_proof (remove_types_env env) prf;
 
 
-(**** substitution of bound variables ****)
+(* substitution of bound variables *)
 
 fun prf_subst_bounds args prf =
   let
@@ -700,7 +701,7 @@
   in (case args of [] => prf | _ => substh prf 0 0) end;
 
 
-(**** Freezing and thawing of variables in proof terms ****)
+(* freezing and thawing of variables in proof terms *)
 
 local
 
@@ -761,7 +762,8 @@
 end;
 
 
-(**** proof terms as pure terms ****)
+
+(** proof terms as pure terms **)
 
 val proofT = Type ("Pure.proof", []);
 
@@ -813,7 +815,10 @@
 end;
 
 
-(***** implication introduction *****)
+
+(** inference rules **)
+
+(* implication introduction *)
 
 fun gen_implies_intr_proof f h prf =
   let
@@ -834,7 +839,7 @@
 val implies_intr_proof' = gen_implies_intr_proof SOME;
 
 
-(***** forall introduction *****)
+(* forall introduction *)
 
 fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf);
 
@@ -843,7 +848,7 @@
   in Abst (a, SOME T, prf_abstract_over t prf) end;
 
 
-(***** varify *****)
+(* varify *)
 
 fun varify_proof t fixed prf =
   let
@@ -887,7 +892,7 @@
 end;
 
 
-(***** rotate assumptions *****)
+(* rotate assumptions *)
 
 fun rotate_proof Bs Bi m prf =
   let
@@ -903,7 +908,7 @@
   end;
 
 
-(***** permute premises *****)
+(* permute premises *)
 
 fun permute_prems_proof prems j k prf =
   let val n = length prems
@@ -912,7 +917,7 @@
   end;
 
 
-(***** generalization *****)
+(* generalization *)
 
 fun generalize (tfrees, frees) idx =
   Same.commit (map_proof_terms_same
@@ -920,7 +925,7 @@
     (Term_Subst.generalizeT_same tfrees idx));
 
 
-(***** instantiation *****)
+(* instantiation *)
 
 fun instantiate (instT, inst) =
   Same.commit (map_proof_terms_same
@@ -928,7 +933,7 @@
     (Term_Subst.instantiateT_same instT));
 
 
-(***** lifting *****)
+(* lifting *)
 
 fun lift_proof Bi inc prop prf =
   let
@@ -980,7 +985,7 @@
     (Logic.incr_indexes_same ([], [], i)) (Logic.incr_tvar_same i));
 
 
-(***** proof by assumption *****)
+(* proof by assumption *)
 
 fun mk_asm_prf t i m =
   let
@@ -996,7 +1001,7 @@
     map PBound (length Bs - 1 downto 0) @ [mk_asm_prf Bi n ~1]));
 
 
-(***** Composition of object rule with proof state *****)
+(* composition of object rule with proof state *)
 
 fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) =
       AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k))
@@ -1018,7 +1023,8 @@
   end;
 
 
-(***** axioms for equality *****)
+
+(** axioms for equality **)
 
 val aT = TFree ("'a", []);
 val bT = TFree ("'b", []);
@@ -1103,7 +1109,8 @@
   equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2;
 
 
-(**** type classes ****)
+
+(** type classes **)
 
 fun strip_shyps_proof algebra present witnessed extra_sorts prf =
   let
@@ -1174,7 +1181,7 @@
 end;
 
 
-(***** axioms and theorems *****)
+(** axioms and theorems **)
 
 val proofs = Unsynchronized.ref 2;
 fun proofs_enabled () = ! proofs >= 2;
@@ -1312,12 +1319,12 @@
   in fn prf => #4 (shrink [] 0 prf) end;
 
 
-(**** Simple first order matching functions for terms and proofs ****)
+
+(** simple first order matching functions for terms and proofs **)
+(*see pattern.ML*)
 
 exception PMatch;
 
-(** see pattern.ML **)
-
 fun flt (i: int) = filter (fn n => n < i);
 
 fun fomatch Ts tymatch j instsp p =
@@ -1461,7 +1468,8 @@
   end;
 
 
-(**** rewriting on proof terms ****)
+
+(** rewriting on proof terms **)
 
 val no_skel = PBound 0;
 val normal_skel = Hyp (Var ((Name.uu, 0), propT));
@@ -1553,7 +1561,8 @@
 fun rewrite_proof_notypes rews = rewrite_prf fst rews;
 
 
-(**** theory data ****)
+
+(** theory data **)
 
 structure Data = Theory_Data
 (
@@ -1575,7 +1584,8 @@
 fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p));
 
 
-(***** promises *****)
+
+(** promises **)
 
 fun promise_proof thy i prop =
   let
@@ -1624,7 +1634,8 @@
   end;
 
 
-(***** abstraction over sort constraints *****)
+
+(** abstraction over sort constraints **)
 
 fun unconstrainT_prf thy (atyp_map, constraints) =
   let
@@ -1649,7 +1660,8 @@
     proof = unconstrainT_prf thy constrs proof};
 
 
-(***** theorems *****)
+
+(** theorems **)
 
 fun prepare_thm_proof thy name shyps hyps concl promises body =
   let