src/Pure/conjunction.ML
changeset 24241 424cb8b5e5b4
parent 23535 58147e5bd070
child 24976 821628d16552
     1.1 --- a/src/Pure/conjunction.ML	Mon Aug 13 12:56:03 2007 +0200
     1.2 +++ b/src/Pure/conjunction.ML	Mon Aug 13 18:10:18 2007 +0200
     1.3 @@ -29,8 +29,8 @@
     1.4  
     1.5  (** abstract syntax **)
     1.6  
     1.7 -fun read s = Thm.read_cterm ProtoPure.thy (s, propT);
     1.8  val cert = Thm.cterm_of ProtoPure.thy;
     1.9 +val read_prop = cert o SimpleSyntax.read_prop;
    1.10  
    1.11  val true_prop = cert Logic.true_prop;
    1.12  val conjunction = cert Logic.conjunction;
    1.13 @@ -63,11 +63,11 @@
    1.14  
    1.15  local
    1.16  
    1.17 -val A = read "PROP A" and vA = read "PROP ?A";
    1.18 -val B = read "PROP B" and vB = read "PROP ?B";
    1.19 -val C = read "PROP C";
    1.20 -val ABC = read "PROP A ==> PROP B ==> PROP C";
    1.21 -val A_B = read "PROP ProtoPure.conjunction(A, B)"
    1.22 +val A = read_prop "A" and vA = read_prop "?A";
    1.23 +val B = read_prop "B" and vB = read_prop "?B";
    1.24 +val C = read_prop "C";
    1.25 +val ABC = read_prop "A ==> B ==> C";
    1.26 +val A_B = read_prop "A && B";
    1.27  
    1.28  val conjunction_def = Drule.unvarify ProtoPure.conjunction_def;
    1.29  
    1.30 @@ -125,7 +125,7 @@
    1.31    let val As = map (fn A => cert (Free (A, propT))) (Name.invents Name.context "A" n)
    1.32    in (As, mk_conjunction_balanced As) end;
    1.33  
    1.34 -val B = cert (Free ("B", propT));
    1.35 +val B = read_prop "B";
    1.36  
    1.37  fun comp_rule th rule =
    1.38    Thm.adjust_maxidx_thm ~1 (th COMP