equal
deleted
inserted
replaced
7 imports Pure |
7 imports Pure |
8 begin |
8 begin |
9 |
9 |
10 section \<open>Constructive Type Theory: axiomatic basis\<close> |
10 section \<open>Constructive Type Theory: axiomatic basis\<close> |
11 |
11 |
12 ML_file "~~/src/Provers/typedsimp.ML" |
12 ML_file \<open>~~/src/Provers/typedsimp.ML\<close> |
13 setup Pure_Thy.old_appl_syntax_setup |
13 setup Pure_Thy.old_appl_syntax_setup |
14 |
14 |
15 typedecl i |
15 typedecl i |
16 typedecl t |
16 typedecl t |
17 typedecl o |
17 typedecl o |
453 Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s)) |
453 Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (NE_tac ctxt s)) |
454 \<close> |
454 \<close> |
455 method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close> |
455 method_setup pc = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (pc_tac ctxt ths))\<close> |
456 method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close> |
456 method_setup add_mp = \<open>Scan.succeed (SIMPLE_METHOD' o add_mp_tac)\<close> |
457 |
457 |
458 ML_file "rew.ML" |
458 ML_file \<open>rew.ML\<close> |
459 method_setup rew = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (rew_tac ctxt ths))\<close> |
459 method_setup rew = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (rew_tac ctxt ths))\<close> |
460 method_setup hyp_rew = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_rew_tac ctxt ths))\<close> |
460 method_setup hyp_rew = \<open>Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_rew_tac ctxt ths))\<close> |
461 |
461 |
462 |
462 |
463 subsection \<open>The elimination rules for fst/snd\<close> |
463 subsection \<open>The elimination rules for fst/snd\<close> |