src/HOL/Tools/SMT/z3_proof_tools.ML
changeset 41123 3bb9be510a9d
parent 40806 59d96f777da3
child 41172 a17c2d669c40
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Dec 15 08:39:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Dec 15 08:39:24 2010 +0100
     1.3 @@ -6,18 +6,18 @@
     1.4  
     1.5  signature Z3_PROOF_TOOLS =
     1.6  sig
     1.7 -  (* accessing and modifying terms *)
     1.8 +  (*accessing and modifying terms*)
     1.9    val term_of: cterm -> term
    1.10    val prop_of: thm -> term
    1.11    val as_meta_eq: cterm -> cterm
    1.12  
    1.13 -  (* theorem nets *)
    1.14 +  (*theorem nets*)
    1.15    val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
    1.16    val net_instance': ((thm -> thm option) -> 'a -> 'a option) -> 'a Net.net ->
    1.17      cterm -> 'a option
    1.18    val net_instance: thm Net.net -> cterm -> thm option
    1.19  
    1.20 -  (* proof combinators *)
    1.21 +  (*proof combinators*)
    1.22    val under_assumption: (thm -> thm) -> cterm -> thm
    1.23    val with_conv: conv -> (cterm -> thm) -> cterm -> thm
    1.24    val discharge: thm -> thm -> thm
    1.25 @@ -29,16 +29,16 @@
    1.26    val by_abstraction: bool * bool -> Proof.context -> thm list ->
    1.27      (Proof.context -> cterm -> thm) -> cterm -> thm
    1.28  
    1.29 -  (* a faster COMP *)
    1.30 +  (*a faster COMP*)
    1.31    type compose_data
    1.32    val precompose: (cterm -> cterm list) -> thm -> compose_data
    1.33    val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
    1.34    val compose: compose_data -> thm -> thm
    1.35  
    1.36 -  (* unfolding of 'distinct' *)
    1.37 +  (*unfolding of 'distinct'*)
    1.38    val unfold_distinct_conv: conv
    1.39  
    1.40 -  (* simpset *)
    1.41 +  (*simpset*)
    1.42    val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
    1.43    val make_simpset: Proof.context -> thm list -> simpset
    1.44  end
    1.45 @@ -107,7 +107,11 @@
    1.46  
    1.47  fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
    1.48  
    1.49 -(* |- c x == t x ==> P (c x)  ~~>  c == t |- P (c x) *) 
    1.50 +(*
    1.51 +   |- c x == t x ==> P (c x)
    1.52 +  ---------------------------
    1.53 +      c == t |- P (c x)
    1.54 +*) 
    1.55  fun make_hyp_def thm ctxt =
    1.56    let
    1.57      val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)