src/Provers/classical.ML
changeset 32862 1fc86cec3bdf
parent 32740 9dd0a2f83429
child 32863 5e8cef567042
equal deleted inserted replaced
32861:105f40051387 32862:1fc86cec3bdf
   694 
   694 
   695 (*** Unsafe steps instantiate variables or lose information ***)
   695 (*** Unsafe steps instantiate variables or lose information ***)
   696 
   696 
   697 (*Backtracking is allowed among the various these unsafe ways of
   697 (*Backtracking is allowed among the various these unsafe ways of
   698   proving a subgoal.  *)
   698   proving a subgoal.  *)
   699 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   699 fun inst0_step_tac (CS {safe0_netpair, ...}) =
   700   assume_tac                      APPEND'
   700   assume_tac APPEND'
   701   contr_tac                       APPEND'
   701   contr_tac APPEND'
   702   biresolve_from_nets_tac safe0_netpair;
   702   biresolve_from_nets_tac safe0_netpair;
   703 
   703 
   704 (*These unsafe steps could generate more subgoals.*)
   704 (*These unsafe steps could generate more subgoals.*)
   705 fun instp_step_tac (CS{safep_netpair,...}) =
   705 fun instp_step_tac (CS {safep_netpair, ...}) =
   706   biresolve_from_nets_tac safep_netpair;
   706   biresolve_from_nets_tac safep_netpair;
   707 
   707 
   708 (*These steps could instantiate variables and are therefore unsafe.*)
   708 (*These steps could instantiate variables and are therefore unsafe.*)
   709 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   709 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   710 
   710 
   908 (** concrete syntax of attributes **)
   908 (** concrete syntax of attributes **)
   909 
   909 
   910 val introN = "intro";
   910 val introN = "intro";
   911 val elimN = "elim";
   911 val elimN = "elim";
   912 val destN = "dest";
   912 val destN = "dest";
   913 val ruleN = "rule";
       
   914 
   913 
   915 val setup_attrs =
   914 val setup_attrs =
   916   Attrib.setup @{binding swapped} (Scan.succeed swapped)
   915   Attrib.setup @{binding swapped} (Scan.succeed swapped)
   917     "classical swap of introduction rule" #>
   916     "classical swap of introduction rule" #>
   918   Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
   917   Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)