src/Pure/drule.ML
changeset 4789 9cf0073bbe2b
parent 4713 bea2ab2e360b
child 5079 2a8ed71f791f
equal deleted inserted replaced
4788:b54c337f2c7f 4789:9cf0073bbe2b
    68   val revcut_rl		: thm
    68   val revcut_rl		: thm
    69   val thin_rl		: thm
    69   val thin_rl		: thm
    70   val triv_forall_equality: thm
    70   val triv_forall_equality: thm
    71   val swap_prems_rl     : thm
    71   val swap_prems_rl     : thm
    72   val equal_intr_rule   : thm
    72   val equal_intr_rule   : thm
       
    73   val triv_goal: thm
       
    74   val rev_triv_goal: thm
    73   val instantiate': ctyp option list -> cterm option list -> thm -> thm
    75   val instantiate': ctyp option list -> cterm option list -> thm -> thm
    74 end;
    76 end;
    75 
    77 
    76 structure Drule : DRULE =
    78 structure Drule : DRULE =
    77 struct
    79 struct
   569     store_thm "equal_intr_rule"
   571     store_thm "equal_intr_rule"
   570       (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   572       (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   571   end;
   573   end;
   572 
   574 
   573 
   575 
       
   576 (* GOAL (PROP A) <==> PROP A *)
       
   577 
       
   578 local
       
   579   val A = read_prop "PROP A";
       
   580   val G = read_prop "GOAL (PROP A)";
       
   581   val (G_def, _) = freeze_thaw ProtoPure.Goal_def;
       
   582 in
       
   583   val triv_goal = store_thm "triv_goal" (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume A));
       
   584   val rev_triv_goal = store_thm "rev_triv_goal" (Thm.equal_elim G_def (Thm.assume G));
       
   585 end;
       
   586 
       
   587 
   574 
   588 
   575 (** instantiate' rule **)
   589 (** instantiate' rule **)
   576 
   590 
   577 (* collect vars *)
   591 (* collect vars *)
   578 
   592