# HG changeset patch # User oheimb # Date 830271711 -7200 # Node ID 33aff4d854e49e0b6b21a59e86810390f68e71d1 # Parent d22110ddd0af1841fc4ad02c196071b0ba6cb30a *** empty log message *** diff -r d22110ddd0af -r 33aff4d854e4 index.html --- a/index.html Tue Apr 23 16:58:57 1996 +0200 +++ b/index.html Tue Apr 23 17:01:51 1996 +0200 @@ -1,6 +1,8 @@ Isabelle Logics

Isabelle Logics

Click on the logic's name to view a list of its theories. + + +
Higher-Order Logic + + +
+ diff -r d22110ddd0af -r 33aff4d854e4 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Apr 23 16:58:57 1996 +0200 +++ b/src/HOL/HOL.thy Tue Apr 23 17:01:51 1996 +0200 @@ -143,40 +143,6 @@ if_def "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)" (* start 8bit 1 *) -types -('a, 'b) "ë" (infixr 5) - -syntax - "Ú" :: "['a::{}, 'a] => prop" ("(_ Ú/ _)" [3, 2] 2) - "êë" :: "[prop, prop] => prop" ("(_ êë/ _)" [2, 1] 1) - "Gbigimpl" :: "[asms, prop] => prop" ("((3Ë _ Ì) êë/ _)" [0, 1] 1) - "Gall" :: "('a => prop) => prop" (binder "Ä" 0) - - "Glam" :: "[idts, 'a::logic] => 'b::logic" ("(3³_./ _)" 10) - "Û" :: "['a, 'a] => bool" (infixl 50) - "Gnot" :: "bool => bool" ("¿ _" [40] 40) - "GEps" :: "[pttrn, bool] => 'a" ("(3®_./ _)" 10) - "GAll" :: "[idts, bool] => bool" ("(3Â_./ _)" 10) - "GEx" :: "[idts, bool] => bool" ("(3Ã_./ _)" 10) - "GEx1" :: "[idts, bool] => bool" ("(3Ã!_./ _)" 10) - "À" :: "[bool, bool] => bool" (infixr 35) - "Á" :: "[bool, bool] => bool" (infixr 30) - "çè" :: "[bool, bool] => bool" (infixr 25) - -translations -(type) "x ë y" == (type) "x => y" - -(* "³x.t" => "%x.t" *) - - "x Û y" == "x ~= y" - "¿ y" == "~y" - "®x.P" == "@x.P" - "Âx.P" == "! x. P" - "Ãx.P" == "? x. P" - "Ã!x.P" == "?! x. P" - "x À y" == "x & y" - "x Á y" == "x | y" - "x çè y" == "x --> y" (* end 8bit 1 *) end @@ -201,36 +167,6 @@ map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")]; (* start 8bit 2 *) -local open Ast; -fun bigimpl_ast_tr (*"Gbigimpl"*) [asms, concl] = - fold_ast_p "êë" (unfold_ast "_asms" asms, concl) - | bigimpl_ast_tr (*"Gbigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts; -fun impl_ast_tr' (*"êë"*) asts = - (case unfold_ast_p "êë" (Appl (Constant "êë" :: asts)) of - (asms as _ :: _ :: _, concl) - => Appl [Constant "Gbigimpl", fold_ast "_asms" asms, concl] - | _ => raise Match); - -in -val parse_ast_translation = ("Gbigimpl", bigimpl_ast_tr):: - ("Glam", fn asts => Appl (Constant "_abs" :: asts)):: - parse_ast_translation; - -val print_ast_translation = ("êë", impl_ast_tr'):: - ("_lambda", fn asts => Appl (Constant "Glam" :: asts)) :: - print_ast_translation; - -end; - -local open Syntax in -val thy = thy -|> add_trrules_i -[mk_appl (Constant "Ú" ) [Variable "P", Variable "Q"] <-> - mk_appl (Constant "==") [Variable "P", Variable "Q"], - mk_appl (Constant "êë" ) [Variable "P", Variable "Q"] <-> - mk_appl (Constant "==>") [Variable "P", Variable "Q"], - (Constant "Ä" ) <-> (Constant "!!")] -end; (* end 8bit 2 *) diff -r d22110ddd0af -r 33aff4d854e4 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Tue Apr 23 16:58:57 1996 +0200 +++ b/src/HOL/Nat.thy Tue Apr 23 17:01:51 1996 +0200 @@ -77,11 +77,6 @@ Least_def "Least(P) == @k. P(k) & (ALL j. j ~P(j))" (* start 8bit 1 *) -syntax - "Gmu" :: (nat => bool) => nat (binder "´" 10) - -translations - "´x.P" == "LEAST x. P" (* end 8bit 1 *) end diff -r d22110ddd0af -r 33aff4d854e4 src/HOL/Prod.thy --- a/src/HOL/Prod.thy Tue Apr 23 16:58:57 1996 +0200 +++ b/src/HOL/Prod.thy Tue Apr 23 17:01:51 1996 +0200 @@ -83,17 +83,6 @@ Unity_def "() == Abs_Unit(True)" (* start 8bit 1 *) -types - -('a, 'b) "ò" (infixr 20) - -translations - -(type) "x ò y" == (type) "x * y" - - "³(x,y,zs).b" == "split(³x.³(y,zs).b)" - "³(x,y).b" == "split(³x y.b)" - (* end 8bit 1 *) end diff -r d22110ddd0af -r 33aff4d854e4 src/HOL/Set.thy --- a/src/HOL/Set.thy Tue Apr 23 16:58:57 1996 +0200 +++ b/src/HOL/Set.thy Tue Apr 23 17:01:51 1996 +0200 @@ -104,33 +104,6 @@ surj_def "surj(f) == ! y. ? x. y=f(x)" (* start 8bit 1 *) -syntax - "Ð" :: "['a set, 'a set] => 'a set" (infixl 70) - "Ñ" :: "['a set, 'a set] => 'a set" (infixl 65) - "Î" :: "['a, 'a set] => bool" (infixl 50) - "ñ" :: "['a, 'a set] => bool" (infixl 50) - GUnion :: "(('a set)set) => 'a set" ("Ó_" [90] 90) - GInter :: "(('a set)set) => 'a set" ("Ò_" [90] 90) - GUNION1 :: "['a => 'b set] => 'b set" (binder "Ó " 10) - GINTER1 :: "['a => 'b set] => 'b set" (binder "Ò " 10) - GINTER :: "[pttrn, 'a set, 'b set] => 'b set" ("(3Ò _Î_./ _)" 10) - GUNION :: "[pttrn, 'a set, 'b set] => 'b set" ("(3Ó _Î_./ _)" 10) - GBall :: "[pttrn, 'a set, bool] => bool" ("(3Â _Î_./ _)" 10) - GBex :: "[pttrn, 'a set, bool] => bool" ("(3Ã _Î_./ _)" 10) - -translations - "x ñ y" == "¿(x : y)" - "x Î y" == "(x : y)" - "x Ð y" == "x Int y" - "x Ñ y" == "x Un y" - "ÒX" == "Inter X" - "ÓX" == "Union X" - "Òx.A" == "INT x.A" - "Óx.A" == "UN x.A" - "ÒxÎA. B" == "INT x:A. B" - "ÓxÎA. B" == "UN x:A. B" - "ÂxÎA. P" == "! x:A. P" - "ÃxÎA. P" == "? x:A. P" (* end 8bit 1 *) end diff -r d22110ddd0af -r 33aff4d854e4 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Tue Apr 23 16:58:57 1996 +0200 +++ b/src/HOLCF/domain/theorems.ML Tue Apr 23 17:01:51 1996 +0200 @@ -45,9 +45,9 @@ in drep end; val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1); -local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in +local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in val kill_neq_tac = dtac trueI2 end; -fun case_UU_tac rews i v = res_inst_tac [("Q",v^"=UU")] classical2 i THEN +fun case_UU_tac rews i v = case_tac (v^"=UU") i THEN asm_simp_tac (HOLCF_ss addsimps rews) i; val chain_tac = REPEAT_DETERM o resolve_tac